-module(prop_cfw).
-include_lib("proper/include/proper.hrl").
-include("../src/rtps.hrl").
-include("../src/rtps_cfw.hrl").

%%%%%%%%%%%%%%%%%%
%%% Properties %%%
%%%%%%%%%%%%%%%%%%
prop_init() ->
    ?FORALL({Min_seq_num, N}, {seq_num(pos_integer()), non_neg_integer()},
        begin
	    %% We get a lost, at least one or more received and an unknown cfws.
	    Cfws = rtps_cfw:new(Min_seq_num, Min_seq_num + N),
	    check_struct_cfws(Cfws, N)
	end).


%%%%%%%%%%%%%%%
%%% Helpers %%%
%%%%%%%%%%%%%%%

%% Check overall structure of the cfws list. N is the number of cfws the list manages.
check_struct_cfws(Cfws, N) ->
    case Cfws of
	[#cfw{status = lost} | Cfws1] ->
	    case lists:last(Cfws1) of
		#cfw{status = unknown} ->
		    Cfws2 = lists:droplast(Cfws1),
		    length(Cfws2) =:= N + 1;
		_ ->
		    false
	    end;
	_ ->
	    false
    end.
    
	
%%%%%%%%%%%%%%%%%%
%%% Generators %%%
%%%%%%%%%%%%%%%%%%
seq_num(Gen) ->
    ?SUCHTHAT(N, Gen, N =/= undefined).
